We now move on to characterize the set of predecessors of a given process (cf. Definition \ref{def:WSTS}) by means of a finite basis (cf. Definition \ref{d:finbas}).
Given a set $S$ of processes, 
we are only interested in those predecessors whose tree is in $\bigset{S}$.
As it will be clear later on, $S$ is intended to represent all processes in a cluster (cf. Definition \ref{d:cluster}).

\begin{definition}
Let $P$ 
and $S$ be an \evold{2} process and a set of \evold{2} processes, respectively.
We define:
$$\Pred_{S}(P) = \{Q \mid Q \in Pred(P),~\Tree(Q) \in \bigset{S} \}.$$
\end{definition}

As we have seen, reductions in \evol{} originate only from synchronizations between input and output prefixes or 
from synchronizations between an adaptable process  and a corresponding update prefix. 
Our characterization of $\Pred_{S}(P)$ as a finite basis relies, intuitively, 
 on the formalization of the 
``parts'' of $P$ that might have been  involved in a reduction leading to $P$. 
We introduce the notion of \emph{syntactic context}: it allows us to reason about the \emph{decompositions} of $P$, which are useful to 
describe the subprocesses that have been involved in the reduction to $P$; 
such subprocesses may be contained in $P$ or they can be found in $S$. 
In the latter case, we must appeal to \emph{parallel extensions} of the syntactic context defining the given decomposition, as we give next:


\begin{definition}[Syntactic Contexts, Decompositions, Extensions]\label{def:SDE}
\emph{Syntactic contexts}, ranged over $K, K', \ldots$, are defined by the following syntax:
\begin{align*}
K ::= [\cdot] ~\mid ~\component{a}{K} ~\mid~ K \parallel K ~\mid~ P
\end{align*}
where $P$ is as in Definition \ref{d:finiteccs} using contexts as in Definition \ref{def:varianti} (2).

Given a process $P$, a syntactic context $K$, and processes $\til R$, we say 
that $K[\tilde{R}]$ is a \emph{decomposition} of $P$ if $P = K[\tilde{R}]$.
%Assume a process $Q$, a syntactic context $K$, and processes $\tilde{R}$.
%If $Q = K[\tilde{R}]$ then we say that $K[\tilde{R}]$ is a \emph{decomposition} of $Q$. 
We assume processes $\tilde{R}$ fill the holes in $K$ preserving the order in which they appear.

A \emph{parallel extension} of $K$ is a syntactic context with exactly two holes obtained in the following way:
$$\mathsf{Ext}(K) = \{K, \, K \parallel  [\cdot], \, K \parallel  [\cdot] \parallel  [\cdot] \} \cap SC_2$$
where $SC_2$ is the set of all syntactic contexts with exactly two holes.
\end{definition}

We move on to define the pred-basis function 
for processes; it is defined with respect to a set of processes $S$ and 
noted $pb_{S}(\cdot)$. First, we present some intuitions and auxiliary definitions.
Given a process $P$, 
%for obtaining 
the set $pb_{S}(P)$ represents the basis for the set $\uparrow \Pred_{S}(\uparrow P)$; 
in other words, it is a finite representation of those processes that reduce  to $P$,
%\todo{removed j from Q not necessary} 
up to $\preceq$, i.e.,  a basis for all those $Q$ such that $Q \pired \succeq P$. 
To this aim,  we consider all the decompositions of 
$P$ as  $K[\til R]$, for some syntactic context $K$ and processes $\til R$, with ${|}\til R{|} \leq 2$.
There are finitely many such decompositions. 
%We will consider extensions of $K_{i}$ with exactly two holes which
%Observe that considering at most two holes 
%is related to the fact that in every reduction two subprocesses are involved. 
%In fact, 
The idea is to characterize a predecessor $Q$ of $P$ by 
%\todo{cambiato qui} properly 
suitably 
filling in the holes in (possibly an extension of) $K$ so that the  $Q$ is such that $\Tree(Q) \in {\cal T}_S$. %focusing on the shape of the subprocesses in $\til R$.
Now, each $K$ can have two, one, or even zero holes (as a process can be a decomposition of itself).
In case ${|}\til R{|} < 2$, the syntactic context must be extended so as to contain exactly two holes; this is defined by $\mathsf{Ext}(K)$ above. % in which the reduction takes place.
%We describe this possible extension next.
%More in details, for each such $K_{i}$, we build a context with exactly two holes, 
%and so a context 
%taken from the set  $\mathsf{Ext}(K)$ is necessary.

Let us analyze the possibilities for such an extended context. 
As we have seen, reductions in \evold{2} arise from the synchronization of two complementary prefixes occurring (i) inside two sums, or (ii) one  inside a sum and the other  in a replicated process;  or (iii) both prefixes  in  two replicated processes. For the sake of readability, and with a little abuse of notation, in the explanation below we use biadic contexts filled in with the interacting prefixes, rather than with the processes in which such prefixes occur. That is, we write $D[\alpha.P, \beta.Q]$ rather than, e.g., $D[\alpha.P + M, !\beta.Q]$.
There are six cases. 
If $K$ has exactly two holes then 
it means that the reduction is ``internal'' to process $P$. 
That is, the reduction can be traced back by looking at  subprocesses of $P$.
Then $P = K[P_1, P_2]$ and 
no parallel extension is needed. There are two possible cases:
%\todo{cambiato qui: aggiunto da dove vengono i pezzetti del predecessore}
\begin{enumerate}
 \item $P$ is the result of an input/output synchronization and so its predecessors are of the form 
 $Q = K[a.P_1, \outC{a}.P_2]$, for some $a \in  \cnames(S)$ and where $a.P_1$ and $\outC{a}.P_2$ are processes in $\subp(S)$.
 
 \item $P$ is the result of a synchronization between an update prefix and some corresponding adaptable process, and so its predecessors are of the form $Q = K[\update{a}{Q'}.P_1, \component{a}{Q''}]$, where $P_2 = \fillcon{Q'}{Q''}$ and $a \in  \cnames(S)$.  
Also, process $\update{a}{Q'}.P_1$ should belong to $\subp(S)$. Moreover, depending on the number of holes in $Q'$ there are two possible situations: (1) if $\numholes{Q'} = 0$ then $P_2 = Q'$ and $Q''$ can be any process in $\subp(S)$; (2) if  $\numholes{Q'} > 0$ then $Q''$ is taken in such a way that $P_2 = \fillcon{Q'}{Q''}$.
\end{enumerate}

In case $K$ has one hole only then we extend the context with a hole so as to accommodate  some process not originally present in $P$. 
That is,  $P = K[P_1]$ and the reduction to $P$ is characterized by  the interaction between 
a prefix guarding subprocess $P_{1}$ 
and some other subprocess external to $P$ (cases (3) and (4) below).
It can also be the case that the reduction is an update synchronization leading to $P_{1}$ (case (5)).
We thus consider the extended context  $D[\cdot,\cdot] \equiv K[\cdot] \parallel [\cdot]$. There are three possible cases:

%Otherwise if $K_i$ has one hole it means that the we obtain a process that is bigger than $Q$ and the synchronization happens between a process that ``contains'' $Q$ and something external to $Q$. The external part is characterized by the parallel extension to the context: i.e. a context $D = K_i \parallel [\cdot]$. There are three situation when this occurs:

\begin{enumerate}
\setcounter{enumi}{2}
 \item $P$ is the result of an input/output synchronization, and so its predecessors are either of the form $Q \equiv D[a.P_1 , \outC{a}.Q_2$] 
 or $Q \equiv D[\outC{a}.P_1, a.Q_2]$, for some $a \in  \cnames(S)$ and processes $a.P_1$ and $\outC{a}.Q_2$ ($\outC{a}.P_1$ and $a.Q_2$, respectively) belong to $\subp(S)$. 
 \item $P$ is the result of a synchronization between an update prefix guarding $P_{1}$ and some corresponding adaptable process, and so its predecessors are of the form $Q \equiv D[\update{a}{Q'}.P_1, \component{a}{Q''}]$, for some $a \in  \cnames(S)$ and with processes $\update{a}{Q'}.P_1$ and $Q''$ in $\subp(S)$.
 \item $P$ is the result of a synchronization between an update prefix and some corresponding adaptable process, 
 in such a way that their synchronization leads to $P_{1}$. This way, 
the predecessors of $P$ are of the form $Q \equiv D[\update{a}{Q'}.Q_2, \component{a}{Q''}]$ or $Q \equiv D[\component{a}{Q''}, \update{a}{Q'}.Q_2]$ where $P_1 = \fillcon{Q'}{Q''}$, for some $a \in  \cnames(S)$. Similarly as in case (2) above, process $\update{a}{Q'}.Q_2$ should belong to $\subp(S)$. Moreover, depending on the number of holes in $Q'$ there are two possible situations: (1) if $\numholes{Q'} = 0$ then $P_1 = Q'$ and $Q''$ can be any process in $\subp(S)$; (2) if  $\numholes{Q'} > 0$ then $Q''$ is taken in such a way that $P_1 = \fillcon{Q'}{Q''}$.
\end{enumerate}
 

The last case to consider is when $K$ has no holes, i.e., the trivial decomposition of $P$ as itself.
Then $D[\cdot,\cdot] \equiv P \parallel [\cdot] \parallel [\cdot] $ and we have:


\begin{enumerate}
\setcounter{enumi}{5}
\item $P$ is the result of a synchronization between the subprocesses in the two added holes.
That is, its predecessors are of one of the following:  
(1) $Q \equiv P \parallel a.R_1 \parallel \outC{a}.R_2 $ and 
(2) $Q \equiv P \parallel \update{a}{Q'}.R_1 \parallel \component{a}{R_{2}} $.
In both cases,  $a \in  \cnames(S)$ and the holes are filled in with processes in $\subp(S)$.%similarly as before.
\end{enumerate}




Before giving the definition of $pb_{S}(Q)$, we introduce an auxiliary notion.
%two auxiliary notions.

\begin{definition}%\label{d:numap}
 Let $P$ be an \evold{2} process.
The set of  update patterns occurring in $P$, denoted 
 $\upd{P}$,  is inductively defined as follows:
$$
\begin{array}{ll}
 \upd{\update{a}{U}.Q} & =  \{U\} \cup \upd{U} \cup \upd{Q}\\  
\upd{\component{a}{P}} &= \upd{P} \\
 \upd{\pi.P} & =  \upd{P} ~~\text{if $\pi = a$ or $\pi = \outC{a}$}\\
 \upd{\sum_{i \in I}\pi_{i}.U_{i}} &= \bigcup_{i \in I}\upd{\pi_{i}.U_{i}} \\  
  \upd{! \pi.U} &= \upd{\pi. U} \\
\upd{U_{1} \parallel U_{2}} & =  \upd{U_{1}} \cup \upd{U_{2}} \\
\upd{\bullet} & = \emptyset 
\end{array}
$$
 This definition extends to sets of processes as expected.
 \end{definition}

%\todo{messy explanation}
%Next, we introduce a minimization function, that, given a set $S$ of processes, removes all those processes that according to the ordering $\preceq$ are bigger than other ones  in the set.
%Given a set of processes $A$, the following definition characterizes the minimal subset of $A$ by ignoring all those elements 
%in $A$ which are greater than an element already in $A$ w.r.t. $\preceq$:

%\begin{definition}\label{def:minim}
%Given a set of processes $A$, its \emph{minimal set (with respect to  $\preceq$)}, is defined as:
%$$ \mathsf{min}_{\preceq}(A)  = A - \{R' \in A \mid R \preceq R', ~ R \in A\}$$
%\end{definition}



 
%Given an \evold{2} process $P$, 
%below we write $\mathsf{Upd}(P)$ to stand for the set
%of update contexts in $P$, i.e., 
%$\mathsf{Upd}(P)=\{U \mid \text{$\update{a}{U}$ occurs in $P$}\}$. 
%This notation extends to sets of processes in the expected way.

\begin{definition}[Pred-basis]\label{d:predbasis}
 Let $S$ be a set of  \evold{2} processes and $P$ be an \evold{2} process such that $\Tree(P)\in \bigset{S}$. 
 %and let $\Tree(Q)$ be a tree over $\bigset{P}$. 
% Let $D, D'$ range over $\xevol$. 
Given the set 
\begin{align*}
\mathcal{G}_{S, \widetilde{R}}  = & ~~\subp(S) \,  \cup \{  \component{a}{H} \mid a\in \cnames(S), ~ H \in \subp(S)\} \, \cup \\
& \qquad ~~~\quad \quad \{\component{a}{H} \mid R=\fillcon{U}{H}, ~R \in \widetilde{R}, ~U \in \mathsf{Upd}(S) , ~\numholes{U} \geq 1 \}
\end{align*}
the \emph{pred-basis of $P$ with respect to $S$}, denoted 
$pb_{S}(P)$, is defined as the set: 
\begin{align*}
pb_{S}(P) & =  %\mathsf{min}_{\preceq}\big(
            \bigcup_{P  = K[\til R]} \big\{  Q \mid   Q \pired \succeq P, ~ Q= D[\til G], ~ D \in \mathsf{Ext}(K),  ~\til G \subseteq   \mathcal{G}_{S, \til{R}} \big\}%\big)
\end{align*}
\end{definition}

We show that the well structured transition system given above has an effective pred-basis (cf. Definition \ref{d:efpb}).


\begin{theorem}\label{th:pbs}
 Let $P$ and $S$ be a \evold{2} process   and a set of  \evold{2} processes, respectively.
 We then have that $\uparrow pb_{S}(P) = \uparrow \Pred_{S}(\uparrow P)$.
Moreover, $pb_{S}(\cdot)$ is effective.
\end{theorem}
\begin{proof}
%\todo{Teorema vero solo se $Q \in S$ o piu debole se tree(Q) in $T_S$!!!!!!}
The inclusion $\uparrow pb_{S}(P) \subseteq \uparrow \Pred_{S}(\uparrow P)$
follows by construction. We consider the other inclusion, i.e.,
$\uparrow \Pred_{S}(\uparrow P) \subseteq \uparrow pb_{S}(P)$.
Given some $R \in \uparrow \Pred_{S}(\uparrow P)$, then 
we show that there is
a $Q \in pb_{S}(P)$ such that $Q \preceq  R$. 
%That is to say, we show that $R \succeq Q \pired \succeq P$, % \todo{the following is wrong} where $R= C[Q]$, for some  monadic context $C$ (cf. Definition \ref{d:mc}).
 As hinted at above, depending on the kind of reduction that can occur to reach process $P$ we should consider six cases. 
% w$Q$ can be obtained by a case analysis on the kind of reductions that can occur to reach a process  greater or equal than $P$. 
%As hinted at above, there are six cases; b
Below,  $K, K_1$ and $K_2$ are syntactic contexts as in Definition \ref{def:SDE}:%, $C$ is a monadic context as in Definition \ref{d:mc}:

%\begin{description}
\paragraph{\bf Reduction is ``internal'' to $P$} Then we have one of the following cases:
\begin{enumerate}
 \item $P$ is obtained as an input/output synchronization. Then, $R = K_1[A, B]$ (or $R = K_1[B,A]$) where $A$ is either 
$!a.Q_1$ or 
$\sum_{i \in I} \pi_i.P_i$ with $\pi_{l}=a$ and $P_l = Q_1$ for some $l\in I$, and 
$B$ is either 
$!\outC{a}.Q_2$
or $\sum_{i \in I} \pi_i.R_i$ with $\pi_{l}=\outC{a}$ and $R_l = Q_2$ , for some $l\in I$.
   There exists $K_2$ such that  $P = K_2[Q_1, Q_2]$ and $R \pired \succeq P$. Since $R \in \uparrow \Pred_{S}(\uparrow P)$ then $A,B \in \subp(S)$  
 %\todo{q: how do we know that they are in $\subp(S)$? does it follow from  $\Tree(Q)\in \bigset{S}$? we need to say this explicitly}
% (respectively $\outC{a}.Q_1, a.Q_2 \in \subp(S)$) 
and we can conclude $R \succeq Q = K_2[A,B] \in pb_S(P)$.
 \item if $P$ is the result of an update of an adaptable process then $$R = K_1[A, \component{a}{Q''}]$$  where $A$ is either 
$!\update{a}{Q'}.Q_1$ or 
$\sum_{i \in I} \pi_i.R_i$ with $\pi_{l}=\update{a}{Q'}$ and $R_l = Q_1$ for some $l\in I$, and there exists $K_2$ such that $P = K_2[Q_1, Q_2]$,  $R \pired \succeq P$ where we have that $Q_2 = \fillcon{Q'}{Q''}$. If $\numholes{Q'} =0$ then $Q_2 = Q'$ and as $R \in \uparrow \Pred_{S}(\uparrow P)$ we have 
$A, Q'' \in \subp(S)$ and  therefore $R \succeq Q =  K_2[A, \component{a}{\nil}] \in  pb_S(P)$. Otherwise if $\numholes{Q'} >0$ then $A \in \subp(S)$ and we can immediately conclude $R \succeq Q =  K_2[A, \component{a}{Q''} \in  pb_S(P)$.
\end{enumerate}

\paragraph{\bf Reduction partially present in $P$} Then we have one of the following cases:
\begin{enumerate}
\setcounter{enumi}{2} 

\item if $R = K_1[A, B]$ (or $R = K_1[B,A]$) where $A$ is either 
$!a.Q_1$ or 
$\sum_{i \in I} \pi_i.P_i$ with $\pi_{l}=a$ and $P_l = Q_1$ for some $l\in I$, and 
$B$ is either 
$!\outC{a}.Q_2$
or $\sum_{i \in I} \pi_i.R_i$ with $\pi_{l}=\outC{a}$ and $R_l = Q_2$ , for some $l\in I$.
Then there exists $K_2$ such that  $P = K_2[Q_1]$ and $R \pired \succeq P$. As $A, B \in \subp(S)$ (respectively $\outC{a}.Q_1, a.Q_2 \in \subp(S)$) we can conclude $R \succeq Q =  K_2[A] \parallel B \in  pb_S(P)$ (respectively $Q = K_2[B] \parallel A$). 

\item if $R = K_1[A, \component{a}{Q_2}]$ where $A$ is either 
$!\update{a}{Q'}.Q_1$ or 
$\sum_{i \in I} \pi_i.R_i$ with $\pi_{l}=\update{a}{Q'}$ and $R_l = Q_1$ for some $l\in I$. Then there exists $K_2$ such that  $P = K_2[Q_1]$ and $R \pired \succeq P$. As  $A \in \subp(S)$ then  $R \succeq Q =  K_2[A] \parallel \component{a}{\nil} \in  pb_S(P)$.

 
\item if $R = K_1[\component{a}{Q''},A$  where $A$ is either 
$!\update{a}{Q'}.Q_2$ or 
$\sum_{i \in I} \pi_i.R_i$ with $\pi_{l}=\update{a}{Q'}$ and $R_l = Q_2$ for some $l\in I$. 
Then there exists $K_2$ such that  $P = K_2[Q_1]$, $R \pired \succeq P$. If $\numholes{Q'} =0$ then $Q_1 = Q'$, $A \in \subp(S)$ and  we can conclude $R \succeq Q =  K_2[\component{a}{\nil}] \parallel A  \in  pb_S(P)$. Otherwise if $\numholes{Q'} >0$ then $Q_1 = \fillcon{Q'}{Q''}$ and we can conclude $R \succeq Q =  K_2[\component{a}{Q''}] \parallel A  \in  pb_S(P)$.
\end{enumerate}

\paragraph{\bf Reduction external to $P$}  Then we have:
\begin{enumerate}
\setcounter{enumi}{5}
 
 \item  $R = K_1[P,  A, B]$ or $R = K_1[P, C, \component{a}{Q_3}]$ where $A$ is either 
$!a.Q_1$ or 
$\sum_{i \in I} \pi_i.P_i$ with $\pi_{l}=a$ and $P_l = Q_1$ for some $l\in I$,  
$B$ is either 
$!\outC{a}.Q_2$
or $\sum_{i \in I} \pi_i.R_i$ with $\pi_{l}=\outC{a}$ and $R_l = Q_2$ , for some $l\in I$ and $C$ is either 
$!\update{a}{Q_1}.Q_2$ or 
$\sum_{i \in I} \pi_i.P_i$ with $\pi_{l}=\update{a}{Q_1}$ and $P_l = Q_2$ for some $l\in I$.
 As all processes $A, B, C, Q_3$ are taken from $\subp(S)$ we can conclude $R \succeq Q =  P \parallel A \parallel B \in  pb_S(P)$ (respectively $Q =  P \parallel C \parallel \component{a}{Q_3} )$.

\end{enumerate}
%\end{description}


Moreover, the construction of $pb_{S}(Q)$ is effective. In particular, given a syntactic context $K$, there are finitely many ways of extending it with one or two holes so as to obtain a parallel extension  $D \in \mathsf{Ext}(K)$.
In Definition \ref{d:predbasis},
notice that when filling in the contexts with terms in $\til G$, both the set of sequential subprocesses and the ways of constructing an update pattern $U$
are finite.
This concludes the proof.
\end{proof}

\begin{theorem}\label{th:fb}
Let $S$ be a set of \evold{2} processes.
%Given $${\cal S}=\{Q \in \evold{2} \mid \Tree(Q) \in \bigset{M}\}$$ then
$ (\deriv{S}, \pired, \preceq)$  is a finitely branching,
well-structured transition system
with strong compatibility, decidable $\preceq$,  and effective pred-basis $pb_S$.
Hence, it is possible to compute a finite basis of $\Pred_{S}^*(I)$ (and $\Pred_{S}^+(I)$) for any upward-closed set $I$
which is given via a finite basis.
\end{theorem}

\begin{proof}
Follows from 
Proposition \ref{predcomp}, using 
Remark \ref{r:fbranch}, and
Theorems \ref{th:scccs} and \ref{th:pbs}.
\end{proof}


%The final step for proving the decidability %of reachability of barbs 
Next, we define the basis of the set of processes that immediately 
exhibit a barb $\alpha$.%, i.e., a finite basis. \todo{not sure this ``id est'' is obvious}

\begin{definition}\label{d:fb1}
 Let $S$ 
 and $\alpha$ 
 be a set of  \evold{2} processes  and a name $\alpha \in \{a, \outC{a} \mid a \in \mathcal{N}\}$, respectively.
%Let $P \in \evold{2}$, $M=\{T_1,\dots,T_n\}$ be a set of terms in \evold{2} and
Then,  we define:
%$S=\{T_1,\dots,T_n\}$ a set of terms in \evold{2}
$$\mathsf{fb}_{\alpha}(S)= \{R \in \subp(S) \mid R \downarrow_{\alpha} \}$$
%The definition is extended to sets of processes in the expected way.
\end{definition}

Given  an initial process $P$, a set of processes $M$,  and a barb $\alpha$, 
to determine whether \OG is decidable, we check if  there exists a process $R \in \BC_P^M$ such that  $R \barb{\alpha}^{k}$. 
It is sufficient to check if $R$ appears in the set of the predecessors of the processes that can exhibit $\alpha$ at least $k$ consecutive times. Since $\preceq$ imposes a well-quasi order on $\evold{2}$ processes, it is enough to characterize the set of predecessors by means of its finite basis, as shown by Theorem \ref{th:fb}.
More precisely, if $k=1$ then it is  sufficient to check if $R$ is in the
set of predecessors of the processes 
in $\mathsf{fb}_{\alpha}(S)$, where $S = M \cup \{P\}$. 
%\todo{up to here, it is not clear how $S$ and $P$ are related...Answer: S here is not related, the discussion is given wrt to a generic process P indipendently of S}
%that can immediately perform $\alpha$. 
Otherwise, if $k>1$ then we need 
%to determine the existence of $k$ evolutions of $R$ with the ability of performing $\alpha$: that is, 
we need to check for the existence of 
processes $R_{1}, \ldots, R_{k}$ such that 
$R \pired^{*} R_1 \pired \dots \pired R_{k}$, with $R_i \xrightarrow{\alpha}$ for $i \in [1..k]$. 
To do this, we proceed backwards. 
We begin by computing the finite basis %of the set of processes that can immediately perform $\alpha$. 
 $\mathsf{fb}_{\alpha}(S)$; process 
$R_{k}$ should be in its upward closure. % of $\mathsf{fb}_{\alpha}(P)$.
Then, 
we compute 
a finite basis for the set of processes in 
$\Pred_{S}(\mathsf{fb}_{\alpha}(S))$ 
%---the set of processes that can perform $\alpha$ ain one or more steps--- 
which exhibit $\alpha$ immediately; $R_{k-1}$ should be in the upward closure of this finite basis, which 
is constructed as follows.
Notice by virtue of Theorem \ref{th:pbs},
 we can rely on the pred-basis given by Definition \ref{d:predbasis}, i.e., $pb_S\big(\mathsf{fb}_{\alpha}(S)\big)$, in this case. 
We consider two classes of elements of $pb_S\big(\mathsf{fb}_{\alpha}(S)\big)$: 
the first one is composed of those processes that can immediately 
perform $\alpha$, while the second contains the rest.
The desired finite basis is obtained by taking %the minimal set 
%w.r.t $\preceq$ (cf. Definition \ref{def:minim}) of 
the set of processes containing 
(i) every process in the first class and 
(ii) every $Q$ in the second class (but with a minimal modification,
with respect to the ordering $\preceq$, 
in such a way it can exhibit $\alpha$ immediately).
The latter is achieved by 
function $\mathsf{Add}_B(Q)$ (cf. Definition \ref{def:fbk})
which ``plugs'' 
into every $Q$ 
a process in $\mathsf{fb}_{\alpha}(S)$ either in parallel at the top level or inside an adaptable process.
%\todo{Check here!}
%every process  $Q \parallel Q'$, where $Q' \in \mathsf{fb}_{\alpha}(S)$ 
This procedure iterates %$k-2$ times; 
as expected; 
each iteration considers the predecessors of the elements of the finite basis obtained in the previous one.
In the last step, in order to calculate all the predecessors of process $R_1$ we apply Theorem \ref{th:fb}, thus obtaining a finite basis where  
 %At this point 
it is
sufficient to check whether $R$ belongs to 
%is in the 
its upward closure. % of the finally obtained basis. 
More formally:

\begin{definition}\label{def:fbk}
 Let $S$ be a  set of  \evold{2} processes. 
%Let $M=\{T_1,\dots,T_n\}$ be a set of terms in \evold{2}, and $P \in \evold{2}$.
Given the following set definitions (with $C$ being a monadic context as in Definition \ref{d:mc})
\begin{align*}
\mathsf{Add}_B(Q) & =  \{Q \parallel R \mid R \in B \} \cup \{C\big[\component{a}{R \parallel Q_{i}}\big] \mid Q = C\big[\component{a}{Q_{i}}\big], ~R \in B\}\\
\mathsf{Ib}_{\alpha}(A, B) & =  \{Q \in A \mid Q \xrightarrow{\alpha} \} \cup \{ \mathsf{Add}_B(Q) \mid Q\in A \text{ and } Q \not \xrightarrow{\alpha}\} %\\
%\mathsf{min}_{\preceq}(A) & = A - \{R' \in A \mid R \preceq R', ~ R \in A\}
\end{align*}
we define the finite basis $\mathsf{FB}_{\alpha,k}(S)= \Pred_S^*(\mathsf{B}_{\alpha,k}(S))$ where $k \geq 1$ and
$$
\mathsf{B}_{\alpha,k}(S) =
\begin{cases}
\mathsf{fb}_{\alpha}(S) & \text{if } k=1\\
%\mathsf{min}_{\procleq}\Big(
\mathsf{Ib}_{\alpha}\Big(pb_S\big(\mathsf{B}_{\alpha, k-1}(S)\big), \mathsf{fb}_{\alpha}\big(S\big)\Big)% \Big)
& \text{otherwise}
\end{cases}
$$
\end{definition}

%\todo{perhaps adding some intuition connecting the previous explanation and the things used in the definition? Answer: yes, i try to to that a bit, we can finish together on friday}
% 
% \todo{
% \begin{definition}
% We define $FB_{\alpha,k}(P,M)= Pred_M^*(FB'_{\alpha,k}(P,M))$ where 
% $$
% FB'_{\alpha,k}(P,M) =
% \begin{cases}
% \mathsf{fb}_{\alpha}(P,M) & \text{if } k=1\\
% \mathsf{Ib}_{\alpha}(pb_M(FB'_{\alpha, k-1}(P,M)), \mathsf{fb}_{\alpha}(P,M)) & \text{otherwise}
% \end{cases}
% $$
% %and both $Pred^*$ and $Pred^+$ are given in terms of finite basis. Moreover, 
% where
% $
% \mathsf{Ib}_{\alpha}(A, B)= \{Q \in A \mid Q \xrightarrow{\alpha} \} \cup \{ \mathsf{Add}_B(Q) \mid Q\in A \text{ and } Q \not \xrightarrow{\alpha}\}
% $ and
%  $\mathsf{Add}_B(Q) =\{Q \parallel R \mid R \in B \} $ is the set of processes obtained by adding in turn, each of the processes in $B$, in parallel at top level or inside every location appearing in $Q$. 
% %\cup \{C[\component{a}{S \parallel R}] \mid  Q = C[\component{a}{S}] \text{ and } R \in B   \}$
% Moreover, to ensure minimality, we  remove from $\mathsf{Ib}_{\alpha}(A, B)$  all $R'$ such that $R \procleq R'$, for some $R$ already in $\mathsf{Ib}_{\alpha}(A, B)$. 
% %And where $Pred'(R)$ is the basis obtained by taking the smallest processes in the union of  all $Pred(R_i)$ for all $R_i \in R$.
% %
% %The definition is extended to sets of processes in the expected way.
%  \end{definition}
% }


The effectiveness of $\mathsf{FB}_{\alpha,k}$ will allow us to prove the decidability of \OG. %, a more formal proof can be found in Appendix \ref{app:decbound}
%


\begin{lemma}\label{lem:decpred}
 Let $S$ be a set of  \evold{2} processes, 
%Let $M=\{T_1,\dots,T_n\}$ be a set of terms in \evold{2}  $P \in \evold{2}$. 
and let $\alpha \in \{a, \outC{a} \mid a \in \mathcal{N}\}$. 
Then, $\mathsf{FB}_{\alpha, k}(S)$ is effective.
\end{lemma}
%\begin{proof}[Sketch]
\begin{proof}
%As hinted at above, checking  whether $P\barb{\alpha}^{k}$ is decidable implies computing the set $FB_{\alpha, k}(P)$.
The effectiveness of the calculation of the finite basis of $\Pred_S^*(\cdot)$ follows from Theorem \ref{th:fb}. 
The set $\mathsf{Ib}_{\alpha}(\cdot,\cdot )$ is finite and hence can be computed as defined above.
Moreover, it is easy to see that it is a finite basis representing all the predecessors of $\mathsf{fb}_{\alpha}(S)$, which in turn can immediately exhibit $\alpha$. %\qed 
\end{proof}

Recall that $\Par(P)$ 
is the set  of all %sequential 
processes 
 and all adaptable processes in $P$ which are 
in parallel at top level (see Definition \ref{d:pps}).
We can finally conclude that:
%


\begin{theorem}\label{th:badec}
\OG  is decidable for \evold{2}.
\end{theorem}
%\begin{proof}[Sketch]
\begin{proof}
Let $P$ and $M=\{T_1, \dots, T_n\}$ be an initial process and a set of \evold{2} processes, respectively.
In order to show that \OG is decidable, it suffices to check 
that, given some $\alpha$ and $k \geq 1$, 
there exists a process $R \in \BC_P^M$ such that $R \barb{\alpha}^{k}$. 
More precisely, letting $S = \{P\} \cup M$, we have to check if there exists a process $Q \in \mathsf{FB}_{\alpha,k}(S)$ such that $Q \preceq R$.
From Lemma \ref{lem:decpred}, we know that it is possible to compute the set $\mathsf{FB}_{\alpha,k}(S)$. %Then depending on the clustering schema the following steps are required.
%
%\todo{not clear to me if the following is the same procedure we describe in the forte paper}
Then, for each $Q_{i}\in \mathsf{FB}_{\alpha,k}(S)$ we analyze the processes in $\mathsf{Par}(Q_{i})$ (cf. Definition \ref{d:pps}). 
Let $V$ be the set of the processes $Q'_{j}$ in $\mathsf{Par}(Q_{i})$
such that $Q_{j}' \preceq T$, for some $T \in M$.
We now consider $Q_{i}^{*}$, the process obtained
by $Q_{i}$ by removing all the occurrences of the parallel
processes in $V$. 
At this point, it is enough to check whether $Q_{i}^{*}\preceq P$. 
If this is the case, for at least one $Q_{i} \in \mathsf{FB}_{\alpha,k}(S)$,
then we can conclude that there exists
$R \in \BC_P^M$ such that $R \barb{\alpha}^{k}$;
otherwise there exists no $R \in \BC_P^M$ such that $R \barb{\alpha}^{k}$.
%\qed
\end{proof}

Notice that 
the decidability result extends to \evold{3}, as it is a subcalculus of  \evold{2}.
Moreover, 
by virtue of Theorems \ref{stdynequiv} and  \ref{th:clusterstat}, 
decidability of \OG extends also to 
\evols{2} and \evols{3}. We then have:
%Since \evold{3} is a subcalculus of \evold{2} and by means of Theorems \ref{stdynequiv} and  \ref{th:clusterstat}, the decidability result extends to \evols{2}, \evold{3}, and \evols{3}.


\begin{corollary}
\OG is decidable for \evold{3}, \evols{2}, and \evols{3}.
\end{corollary}



